(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 1))
(declare-fun v1 () (_ BitVec 13))
(declare-fun v2 () (_ BitVec 7))
(declare-fun v3 () (_ BitVec 2))
(assert (let ((e4(_ bv34269 16)))
(let ((e5 (bvcomp ((_ sign_extend 3) v1) e4)))
(let ((e6 (ite (bvsge v0 e5) (_ bv1 1) (_ bv0 1))))
(let ((e7 (bvnor ((_ sign_extend 14) v3) e4)))
(let ((e8 (ite (bvuge e7 e4) (_ bv1 1) (_ bv0 1))))
(let ((e9 (ite (= (_ bv1 1) ((_ extract 0 0) v2)) ((_ sign_extend 5) v3) v2)))
(let ((e10 (bvslt e7 ((_ zero_extend 15) v0))))
(let ((e11 (distinct e8 v0)))
(let ((e12 (bvsge v1 ((_ zero_extend 12) e6))))
(let ((e13 (bvslt v0 e5)))
(let ((e14 (bvsge v0 e5)))
(let ((e15 (bvugt e9 ((_ zero_extend 6) e6))))
(let ((e16 (bvule ((_ zero_extend 5) v3) v2)))
(let ((e17 (distinct e9 ((_ zero_extend 6) e8))))
(let ((e18 (bvuge e6 e6)))
(let ((e19 (= e6 v0)))
(let ((e20 (bvsgt e9 ((_ sign_extend 6) e5))))
(let ((e21 (bvsle e6 e6)))
(let ((e22 (bvule e8 e8)))
(let ((e23 (bvsle v0 e5)))
(let ((e24 (bvsge e8 v0)))
(let ((e25 (bvsle ((_ zero_extend 6) e6) v2)))
(let ((e26 (bvule ((_ zero_extend 15) e6) e7)))
(let ((e27 (bvult v0 e6)))
(let ((e28 (bvugt ((_ sign_extend 15) e8) e4)))
(let ((e29 (not e12)))
(let ((e30 (ite e14 e13 e17)))
(let ((e31 (and e23 e26)))
(let ((e32 (and e22 e21)))
(let ((e33 (ite e16 e30 e24)))
(let ((e34 (xor e31 e27)))
(let ((e35 (= e32 e29)))
(let ((e36 (and e33 e33)))
(let ((e37 (and e15 e35)))
(let ((e38 (ite e25 e37 e28)))
(let ((e39 (or e10 e36)))
(let ((e40 (and e18 e11)))
(let ((e41 (=> e34 e34)))
(let ((e42 (and e39 e38)))
(let ((e43 (or e41 e40)))
(let ((e44 (=> e20 e42)))
(let ((e45 (= e43 e43)))
(let ((e46 (and e44 e19)))
(let ((e47 (and e45 e46)))
e47
)))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
